consensus.6.jani:model: info: consensus.6 is an MDP model and will be simulated as an MDP.
consensus.6.jani:variables[6]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
consensus.6.jani:variables[8]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
consensus.6.jani:variables[10]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
consensus.6.jani:variables[12]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
consensus.6.jani:variables[14]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
consensus.6.jani:variables[16]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
consensus.6.jani: info: Using default value of 0.95 for the confidence parameter.
consensus.6.jani: warning: Using the Chow-Robbins method for relative-width sequential confidence intervals, which guarantees the requested confidence only asymptotically for decreasing width.
Peak memory usage: 59 MB
Analysis results for consensus.6.jani
Experiment K=2
Status: Finished
Simulation time: 599.5 s
+ Property Property "steps_min"
Estimated min. value: 520.3991843393151
Min. confidence interval: [509.99648495202564, 530.8018837266045]
Runs used (best scheduler): 6130
Total runs used: 1294130
Schedulers sampled: 1000
Best scheduler: 429328836
Run type: MDP
Status: Finished
+ Min. sample data
Mean: 520.3991843393151
Variance: 172685.7056935752
Skewness: 1.8634858638410479
Kurtosis: 8.174441629508395
+ Error bounds
Scheduler sampling: The result is an upper bound for the true min. value.
Statement: CI: 100(1 - α)% of intervals contain true value (CLT assumption)
α: 0.050000000000000044